We introduce Symbolic Alternating Finite Automata (s-AFA) as an expressive,succinct, and decidable model for describing sets of finite sequences overarbitrary alphabets. Boolean operations over s-AFAs have linear complexity,which is in sharp contrast with the quadratic cost of intersection and unionfor non-alternating symbolic automata. Due to this succinctness, emptiness andequivalence checking are PSpace-hard. We introduce an algorithm for checking the equivalence of two s-AFAs based onbisimulation up to congruence. This algorithm allows us to exploit the power ofSAT and SMT solvers to efficiently search the state space of the s-AFAs. Weevaluate our decision procedure on two verification and security applications:1) checking satisfiability of linear temporal logic formulas over finitetraces, and 2) checking equivalence of Boolean combinations of regularexpressions. Our experiments show that our technique often outperforms existingtechniques and it can be beneficial in both such applications.
展开▼
